Accept valid differing solver witnesses; drop ABA shape property deadline - #97
Merged
Merged
Conversation
The helper required identical single-extension witnesses and acceptance
certificates, so native {a} and SAT {c}, both stage extensions, were
reported as a semantic disagreement. Witnesses are choices: differing
ones now agree when each is an extension in reference_extensions (and,
for acceptance, contains or omits the query as required). Answers and
extension existence must still match, and differing witnesses without a
reference set fail with an explicit message.
Closes #73
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01V4tAVyyKcs1sYcsEzL7Bzg
These properties check shape invariants, not speed, but ran under Hypothesis's 200 ms deadline while some generated frameworks take several hundred ms (observed 251-286 ms failures, 0-611 ms typical runtimes), so they failed with DeadlineExceeded under load. The module now uses one settings object with deadline=None and the same max_examples=40; the global Hypothesis default is unchanged. Closes #95 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01V4tAVyyKcs1sYcsEzL7Bzg
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes two issues, one commit each.
#73: solver differential helper rejected different valid witnesses
assert_solver_results_agreerequired both solvers to return the same single-extension witness and the same acceptance certificates. Solvers are allowed to return any valid one. On the stage framework from the issue, native returns{a}and SAT returns{c}, which are both stage extensions (Dvorak et al. 2014, Def 3), yet the helper reported a disagreement.The helper now takes two optional keyword arguments:
reference_extensions, the full set of extensions for the semantics, andquery.reference_extensions.reference_extensionsis needed to judge them.Tests are in
tests/solving/test_solver_differential_witnesses.py:#95: ABA shape property tests failed on the Hypothesis deadline
These property tests check shape invariants, not speed, but they ran under Hypothesis's 200 ms per-example deadline. Some generated frameworks take several hundred milliseconds: observed failures took 214.87, 251.43 and 286.03 ms, and typical runtimes were 0-611 ms. So the tests failed intermittently with
DeadlineExceededwhenever the machine was busy.The module now shares one
settings(max_examples=40, deadline=None)object across its tests.max_examplesis the same as before, and the global Hypothesis default is not changed.Closes #73
Closes #95
🤖 Generated with Claude Code
https://claude.ai/code/session_01V4tAVyyKcs1sYcsEzL7Bzg